g:IGroup, a, b:|g|. (a = b)  (e = (b * (~(a)))  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup
Definitions	t  T, x:A. B(x), True, T, P & Q, P  Q, , P  Q, x f y, P  Q, IMonoid, IGroup
Lemmas	igrp wf, grp car wf, mon ident, grp inverse, mon assoc, true wf, squash wf, iff wf, grp eq op r, grp inv wf, grp op wf, grp id wf, iff functionality wrt iff